package preprocessor.absorption.extended;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import option.KBVocabulary;

import kb.TBox;

import entities.Individual;
import entities.concept.AtomicConcept;
import entities.concept.Concept;
import entities.concept.ExistsConcept;
import entities.concept.PConcept;
import entities.role.Role;
import reasoner.KBReason;
import utils.exception.AbsorptionException;
import utils.exception.ConceptException;
import utils.exception.CoreReasoningException;
import utils.exception.TypeException;

/**
 * Note: if one does existential optimization before universal optimization.
 * Then A -> Some R.B, where B->C, a new assertion b:B is added
 * Later if we see A-> All R.C, and we reuse B to get A-> All R.B, then 
 * B is already realized, i.e., no need to do logical consequence checks.
 *
 * If we do the reverse, we may save the introduction of some new ABox entries 
 * (unlikely I think).
 * 
 * Suggestion: existential first!
 * @author j55wu
 *
 */



public class OptimizedExistentials extends OptimizedRestrictions {
		private static int totalEx = 0,processedex = 0;
		private static Map<Concept, Individual> addedData = 
				new HashMap<Concept, Individual>();
		
		public static final boolean useInconsistencyCheck = true;
		
		public static boolean hasSomeIndividual(Concept c){
			if(realizedInds.containsKey(c) || addedData.containsKey(c)){
				return true;
			}
			return false;
		}
	 
		protected static void addNewABoxData(Concept c) {
			if(addedData.containsKey(c)){
				//here, do not consider realized inds, which are named. Always add anon ind for internal concepts.
				return;
			}
			Individual internal =  Individual.getInternalIndividual();
			addedData.put(c, internal);
			//also add to realized ind
			addRealizedInd(c, internal);
		}
		
		
		public static void addExists(Concept lhs, ExistsConcept rhs) {
			totalEx++;
			Role r = rhs.getRole();
			Map<Concept, Set<Concept>> umap = null;
			if (normalizedExists.containsKey(r)) {
				umap = normalizedExists.get(r);
			} else {
				umap = new HashMap<Concept, Set<Concept>>();
			}
			Concept filler = rhs.getFiller();
			if (umap.containsKey(lhs)) {
				umap.get(lhs).add(filler);
			} else {
				Set<Concept> cs = new HashSet<Concept>();
				cs.add(filler);
				umap.put(lhs, cs);
			}
			normalizedExists.put(r, umap);
		}
		
		private static void addDefr (Role r, PConcept lhs, Concept rhs, TBox tb) 
				throws ConceptException, AbsorptionException{
			//remove original axiom lhs-> some r.rhs from tb (unary)
			ExistsConcept ec = new ExistsConcept(r, rhs);
			tb.removeFromTu(lhs, ec);
			//binary absorb
			PConcept defr = PConcept.newGuardPConcept(r);
			tb.getLessSpecialBinaryClass().addBinaryEntry(defr, lhs, ec);
		}
		
		//assume the given tb is already a converted one
		protected static void optimizeEX(TBox tb)
				throws CoreReasoningException, TypeException, 
				ConceptException, AbsorptionException {
			if(!OptimizedRestrictions.OptimizeEx){
				return;
			}
			long start = System.currentTimeMillis();
			//check and modify existentials
			for(Role r:normalizedExists.keySet()){
				for(Concept lhs:normalizedExists.get(r).keySet()){
					for(Concept filler:normalizedExists.get(r).get(lhs)){
						if(filler.isBot()){
							continue;
						}
						if(canBeProcessed(r, filler)){
							processedex ++;
							addDefr(r, (PConcept) lhs, filler, tb);
						}
					}
				}
			}
			long end = System.currentTimeMillis();
			if (verbose) {
				System.err.println("\n# of existential (A-> some R.B) / processed " + totalEx +"/"+processedex);
				System.err.println("Optimization of existential time: " + ((end - start) * 1.0 / 1000));
			}
			materializeNewData(tb);
		}

		//determine if some r.filler is to be processed
		private static boolean canBeProcessed(Role r, Concept filler){
			if(filler.isTop() || realizedInds.containsKey(filler)){
				return true;
			}
			//the range of r contains the filler
			Concept range = r.getRange();
			if(Concept.reduceToConjuncts(range).contains(filler)){
				//add new data
				addNewABoxData(filler);
				//add to TBox
				return true;
			}
			return false;
		}
		
		private static void materializeNewData(TBox tb) throws TypeException, CoreReasoningException{
			for (Concept c : addedData.keySet()) {
				Individual a = addedData.get(c);
				AssertionConversion.convertCAssertion(a, c, tb);
			}
		}
		
}
